Termination w.r.t. Q proof of /tmp/tmpwY3V2M/PALINDROME_nokinds-noand

Termination w.r.t. Q of the following Term Rewriting System could be disproven:

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X
U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

__(__(X, Y), Z) → __(X, __(Y, Z))
__(X, nil) → X
__(nil, X) → X

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = 2·x₁
POL(U31(x₁)) = 2·x₁
POL(U41(x₁)) = 2·x₁
POL(U42(x₁)) = x₁
POL(U51(x₁)) = x₁
POL(U52(x₁)) = x₁
POL(U61(x₁)) = x₁
POL(U71(x₁)) = 2·x₁
POL(U72(x₁)) = 2·x₁
POL(U81(x₁)) = 2·x₁
POL(__(x₁, x₂)) = 2 + 2·x₁ + x₂
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 0
POL(isPal) = 0
POL(isQid) = 0
POL(nil) = 1
POL(tt) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U61(isQid)
isNePal → U71(isQid)
isPal → U81(isNePal)
isPal → tt
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

isNePal → U61(isQid)
isPal → tt

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = x₁
POL(U31(x₁)) = x₁
POL(U41(x₁)) = 2·x₁
POL(U42(x₁)) = 2·x₁
POL(U51(x₁)) = 2·x₁
POL(U52(x₁)) = 2·x₁
POL(U61(x₁)) = 2·x₁
POL(U71(x₁)) = 1 + 2·x₁
POL(U72(x₁)) = x₁
POL(U81(x₁)) = x₁
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 1
POL(isPal) = 1
POL(isQid) = 0
POL(tt) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U61(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

U61(tt) → tt

Used ordering:
Polynomial interpretation [25]:

POL(U11(x₁)) = 2·x₁
POL(U21(x₁)) = 2·x₁
POL(U22(x₁)) = x₁
POL(U31(x₁)) = x₁
POL(U41(x₁)) = x₁
POL(U42(x₁)) = 2·x₁
POL(U51(x₁)) = 2·x₁
POL(U52(x₁)) = 2·x₁
POL(U61(x₁)) = 1 + x₁
POL(U71(x₁)) = 2·x₁
POL(U72(x₁)) = x₁
POL(U81(x₁)) = 2·x₁
POL(isList) = 0
POL(isNeList) = 0
POL(isNePal) = 0
POL(isPal) = 0
POL(isQid) = 0
POL(tt) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → U72¹(isPal)
ISNELIST → ISNELIST
ISNELIST → ISLIST
ISLIST → ISLIST
U71¹(tt) → ISPAL
ISLIST → ISNELIST
U21¹(tt) → U22¹(isList)
U41¹(tt) → U42¹(isNeList)
U51¹(tt) → U52¹(isList)
ISNELIST → U41¹(isList)
ISPAL → U81¹(isNePal)
ISNEPAL → U71¹(isQid)
U21¹(tt) → ISLIST
ISNELIST → U51¹(isNeList)
U51¹(tt) → ISLIST
U41¹(tt) → ISNELIST
ISLIST → U11¹(isNeList)
ISNELIST → U31¹(isQid)
ISNELIST → ISQID
ISNEPAL → ISQID
ISLIST → U21¹(isList)

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → U72¹(isPal)
ISNELIST → ISNELIST
ISNELIST → ISLIST
ISLIST → ISLIST
U71¹(tt) → ISPAL
ISLIST → ISNELIST
U21¹(tt) → U22¹(isList)
U41¹(tt) → U42¹(isNeList)
U51¹(tt) → U52¹(isList)
ISNELIST → U41¹(isList)
ISPAL → U81¹(isNePal)
ISNEPAL → U71¹(isQid)
U21¹(tt) → ISLIST
ISNELIST → U51¹(isNeList)
U51¹(tt) → ISLIST
U41¹(tt) → ISNELIST
ISLIST → U11¹(isNeList)
ISNELIST → U31¹(isQid)
ISNELIST → ISQID
ISNEPAL → ISQID
ISLIST → U21¹(isList)

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 9 less nodes.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → ISPAL
ISNEPAL → U71¹(isQid)

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We can use the usable rules and reduction pair processor [15] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its argument. Then, we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ MNOCProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → ISPAL
ISNEPAL → U71¹(isQid)

The TRS R consists of the following rules:

isQid → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [15] to enlarge Q to all left-hand sides of R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ MNOCProof

                              ↳ QDP

                                ↳ Rewriting

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → ISPAL
ISNEPAL → U71¹(isQid)

The TRS R consists of the following rules:

isQid → tt

The set Q consists of the following terms:

isQid

We have to consider all minimal (P,Q,R)-chains.
By rewriting [15] the rule ISNEPAL → U71¹(isQid) at position [0] we obtained the following new rules:

ISNEPAL → U71¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ MNOCProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → ISPAL
ISNEPAL → U71¹(tt)

The TRS R consists of the following rules:

isQid → tt

The set Q consists of the following terms:

isQid

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ MNOCProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → ISPAL
ISNEPAL → U71¹(tt)

R is empty.
The set Q consists of the following terms:

isQid

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

isQid

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ MNOCProof

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ UsableRulesProof

                                      ↳ QDP

                                        ↳ QReductionProof

                                          ↳ QDP

                                            ↳ NonTerminationProof

                      ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → ISPAL
ISNEPAL → U71¹(tt)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

ISPAL → ISNEPAL
U71¹(tt) → ISPAL
ISNEPAL → U71¹(tt)

The TRS R consists of the following rules:none

s = ISNEPAL evaluates to t =ISNEPAL

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

ISNEPAL → U71¹(tt)
with rule ISNEPAL → U71¹(tt) at position [] and matcher [ ]

U71¹(tt) → ISPAL
with rule U71¹(tt) → ISPAL at position [] and matcher [ ]

ISPAL → ISNEPAL
with rule ISPAL → ISNEPAL

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → ISNELIST
ISLIST → ISLIST
ISNELIST → ISLIST
ISLIST → ISNELIST
ISNELIST → U51¹(isNeList)
U51¹(tt) → ISLIST
U41¹(tt) → ISNELIST
ISNELIST → U41¹(isList)
ISLIST → U21¹(isList)
U21¹(tt) → ISLIST

The TRS R consists of the following rules:

U11(tt) → tt
U21(tt) → U22(isList)
U22(tt) → tt
U31(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U71(tt) → U72(isPal)
U72(tt) → tt
U81(tt) → tt
isList → U11(isNeList)
isList → tt
isList → U21(isList)
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
isNePal → U71(isQid)
isPal → U81(isNePal)
isQid → tt

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → ISLIST
ISLIST → ISLIST
ISNELIST → ISNELIST
ISLIST → ISNELIST
ISNELIST → U51¹(isNeList)
U51¹(tt) → ISLIST
ISNELIST → U41¹(isList)
U41¹(tt) → ISNELIST
U21¹(tt) → ISLIST
ISLIST → U21¹(isList)

The TRS R consists of the following rules:

isList → U11(isNeList)
isList → tt
isList → U21(isList)
U21(tt) → U22(isList)
U22(tt) → tt
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U11(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U51¹(isNeList) at position [0] we obtained the following new rules:

ISNELIST → U51¹(U51(isNeList))
ISNELIST → U51¹(U41(isList))
ISNELIST → U51¹(U31(isQid))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U51¹(U51(isNeList))
ISNELIST → ISLIST
ISLIST → ISLIST
ISNELIST → ISNELIST
ISLIST → ISNELIST
ISNELIST → U51¹(U41(isList))
ISNELIST → U41¹(isList)
U21¹(tt) → ISLIST
ISNELIST → U51¹(U31(isQid))
U51¹(tt) → ISLIST
U41¹(tt) → ISNELIST
ISLIST → U21¹(isList)

The TRS R consists of the following rules:

isList → U11(isNeList)
isList → tt
isList → U21(isList)
U21(tt) → U22(isList)
U22(tt) → tt
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U11(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U41¹(isList) at position [0] we obtained the following new rules:

ISNELIST → U41¹(U21(isList))
ISNELIST → U41¹(tt)
ISNELIST → U41¹(U11(isNeList))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U51¹(U51(isNeList))
ISNELIST → ISNELIST
ISLIST → ISLIST
ISNELIST → ISLIST
ISNELIST → U41¹(U11(isNeList))
ISLIST → ISNELIST
ISNELIST → U51¹(U41(isList))
U21¹(tt) → ISLIST
ISNELIST → U41¹(U21(isList))
ISNELIST → U51¹(U31(isQid))
U51¹(tt) → ISLIST
ISNELIST → U41¹(tt)
U41¹(tt) → ISNELIST
ISLIST → U21¹(isList)

The TRS R consists of the following rules:

isList → U11(isNeList)
isList → tt
isList → U21(isList)
U21(tt) → U22(isList)
U22(tt) → tt
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U11(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISLIST → U21¹(isList) at position [0] we obtained the following new rules:

ISLIST → U21¹(U21(isList))
ISLIST → U21¹(tt)
ISLIST → U21¹(U11(isNeList))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U51¹(U51(isNeList))
ISNELIST → ISLIST
ISLIST → ISLIST
ISNELIST → ISNELIST
ISLIST → ISNELIST
ISNELIST → U41¹(U11(isNeList))
ISLIST → U21¹(U11(isNeList))
ISNELIST → U51¹(U41(isList))
ISLIST → U21¹(U21(isList))
U21¹(tt) → ISLIST
ISNELIST → U41¹(U21(isList))
ISNELIST → U51¹(U31(isQid))
U51¹(tt) → ISLIST
U41¹(tt) → ISNELIST
ISNELIST → U41¹(tt)
ISLIST → U21¹(tt)

The TRS R consists of the following rules:

isList → U11(isNeList)
isList → tt
isList → U21(isList)
U21(tt) → U22(isList)
U22(tt) → tt
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U11(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U51¹(U31(isQid)) at position [0] we obtained the following new rules:

ISNELIST → U51¹(U31(tt))

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U51¹(U31(tt))
ISNELIST → U51¹(U51(isNeList))
ISNELIST → ISNELIST
ISLIST → ISLIST
ISNELIST → ISLIST
ISNELIST → U41¹(U11(isNeList))
ISLIST → ISNELIST
ISLIST → U21¹(U11(isNeList))
ISNELIST → U51¹(U41(isList))
ISLIST → U21¹(U21(isList))
U21¹(tt) → ISLIST
ISNELIST → U41¹(U21(isList))
U51¹(tt) → ISLIST
ISNELIST → U41¹(tt)
U41¹(tt) → ISNELIST
ISLIST → U21¹(tt)

The TRS R consists of the following rules:

isList → U11(isNeList)
isList → tt
isList → U21(isList)
U21(tt) → U22(isList)
U22(tt) → tt
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U11(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule ISNELIST → U51¹(U31(tt)) at position [0] we obtained the following new rules:

ISNELIST → U51¹(tt)

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ DependencyPairsProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ AND

                      ↳ QDP

                      ↳ QDP

                        ↳ UsableRulesProof

                          ↳ QDP

                            ↳ Narrowing

                              ↳ QDP

                                ↳ Narrowing

                                  ↳ QDP

                                    ↳ Narrowing

                                      ↳ QDP

                                        ↳ Narrowing

                                          ↳ QDP

                                            ↳ Narrowing

                                              ↳ QDP

                                                ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

ISNELIST → U51¹(U51(isNeList))
ISNELIST → ISLIST
ISLIST → ISLIST
ISNELIST → ISNELIST
ISLIST → ISNELIST
ISNELIST → U41¹(U11(isNeList))
ISLIST → U21¹(U11(isNeList))
ISNELIST → U51¹(U41(isList))
ISLIST → U21¹(U21(isList))
U21¹(tt) → ISLIST
ISNELIST → U41¹(U21(isList))
ISNELIST → U51¹(tt)
U51¹(tt) → ISLIST
U41¹(tt) → ISNELIST
ISNELIST → U41¹(tt)
ISLIST → U21¹(tt)

The TRS R consists of the following rules:

isList → U11(isNeList)
isList → tt
isList → U21(isList)
U21(tt) → U22(isList)
U22(tt) → tt
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U11(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

ISNELIST → U51¹(U51(isNeList))
ISNELIST → ISLIST
ISLIST → ISLIST
ISNELIST → ISNELIST
ISLIST → ISNELIST
ISNELIST → U41¹(U11(isNeList))
ISLIST → U21¹(U11(isNeList))
ISNELIST → U51¹(U41(isList))
ISLIST → U21¹(U21(isList))
U21¹(tt) → ISLIST
ISNELIST → U41¹(U21(isList))
ISNELIST → U51¹(tt)
U51¹(tt) → ISLIST
U41¹(tt) → ISNELIST
ISNELIST → U41¹(tt)
ISLIST → U21¹(tt)

The TRS R consists of the following rules:

isList → U11(isNeList)
isList → tt
isList → U21(isList)
U21(tt) → U22(isList)
U22(tt) → tt
isNeList → U31(isQid)
isNeList → U41(isList)
isNeList → U51(isNeList)
U11(tt) → tt
U51(tt) → U52(isList)
U52(tt) → tt
U41(tt) → U42(isNeList)
U42(tt) → tt
isQid → tt
U31(tt) → tt

s = ISLIST evaluates to t =ISLIST

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from ISLIST to ISLIST.